Solovay Sentencesの構成
以下は証明抜きで使うことにしよう．
$ Fを$ n+1変数の原始再帰関数とする．
このとき，原始再帰関数のコード$ eがあって，$ \{e\}(\vec{x}) = F(e, \vec{x})となる．
ただし$ \{e\}は$ eをコードとして持つ関数とする．（この場合は更に原始再帰関数）
proof
Prelim
$ \mathbf{GL} \nvdash Aだとする．このとき$ \bf GL木モデル$ \mathcal{M} = \lang W,R,0,V \rangがあって特にその根$ 0で$ \mathcal{M},0 \nvDash A．
$ W = \{0,1,\dots,n\}とする．
おそらく？もっと正確には$ \mathcal{M}が$ W \sube \Nである保証は無いが，木の構造を全く同じに保ちながら自然数上$ Wの木に変形してもその妥当性は保存される．
よって，$ Wは自然数上のものとしてよい．
$ \lnot \exists_{m} \forall_{n > m}.\lbrack f_h(n) = \bar{z} \rbrackという論理式を考える．
ここで$ f_hは$ hという関数のコードに算術の言語上で対応する関数記号とする．
すなわち
$ h: 関数のコード
$ \{h\}: 関数
$ f_h: 関数$ \{h\}に対応する算術の言語上の関数記号
この論理式のGödel数を計算する原始再帰関数を$ G_z(h)とする．すなわち
$ G_z(h) \equiv \ulcorner \lnot \exists_{m} \forall_{n > m}.\lbrack f_h(n) = \bar{z} \rbrack \urcorner
次に，原始再帰関数$ F(h,n,y)を次のように定める．
$ F(h,n,y) = z：ある$ y R zな$ zが存在し，$ \mathbf{PA} \vdash \mathrm{Prov}_T(n, G_z(h))
すなわち，$ nが$ T上の証明のコードで，その証明の最後の論理式は$ G_z(h)のコードと同じ
$ F(h,n,y) = y：それ以外
次に，原始再帰関数$ K(h,n)を次のように定める．
1. $ K(h,0) = 0
2. $ K(h, n+1) = F(h,n,K(h,n))
最後に，$ Kに対して再帰定理より，次のような原始再帰関数のコード$ hが存在する． $ \{h\}(n) = K(h,n)
さて，この関数$ \{h\}を$ Hとする．$ Hの挙動を調べるとこうなる
1. $ H(0) = K(h, 0) = 0
2. $ H(n+1) = K(h, n+1) = F(h,n,K(h,n))
$ F(h,n,K(h,n)) = z：ある$ K(h,n)Rzな$ zが存在して$ \mathbf{PA} \vdash \mathrm{Prov}_T(n, G_z(h))
$ F(h,n,K(h,n)) = K(h,n) = H(n)
さて今$ K(h,n)とは$ H(n)のことだったから，纏め直すと
$ H(n+1) = z：ある$ H(n) R zな$ zが存在して$ \mathbf{PA} \vdash \mathrm{Prov}_T(n, G_z(h))
$ H(n+1) = H(n)：それ以外
$ \mathrm{Prov}_T(n, G_z(h))を考えると，
$ G_z(h) \equiv \ulcorner \lnot \exists_{m} \forall_{n > m}.\lbrack f_h(n) = \bar{z} \rbrack \urcornerで$ f_hというのは$ \{h\}すなわち$ Hに対応する関数記号だった．
$ \lnot以降の$ \exists_{m} \forall_{n > m}.\lbrack f_h(n) = \bar{z} \rbrackの部分の論理式（文）を$ \beta_zとする．
$ G_z(h) \equiv \ulcorner \lnot \beta_z \urcornerとなる．
すなわち，$ \lnot \beta_zの証明のGödel数が$ nであるとき，$ H(n + 1) = zとなる．
$ \beta_z \equiv \exists_{m} \forall_{n > m}.\lbrack f_h(n) = \bar{z} \rbrackについて直感的な説明を与えておくと，
ある$ mが存在して，$ mよりどれだけ大きな$ nをとってきても$ H(n) = zとなる．
すなわち，関数$ Hには極限値が存在して，それが$ z \in Wであるということを主張している．
「$ \bf PA上で$ Hの極限値が$ zでないことが（特にコード$ nを持つ証明によって）証明できた」とき，$ H(n + 1) = zに値が更新される．
さて，ここまで定義してきたにも関わらず，$ H(n)の極限値は実際には更新されることなく，任意の$ nで$ H(n) = 0である．
背理法．もし更新されたとして，$ 0 R z_0かつ$ H(n_0 + 1) = z_0になったとする．
このとき更新できたということは$ z_0は$ Hの極限値ではないことが証明されている，すなわち，いつか$ n_0 < n_1となる$ n_1によって$ H(n_1 + 1) = z_1に値が更新されなければならない．そして定義より$ z_0 R z_1である．
この手続きを繰り返していくと$ Wは有限だから，$ z_m R z_{m+1}となる$ z_{m+1}が存在しない終末$ z_mに更新される時がやってくる．
この$ z_mについても，$ Hの極限値は$ z_mでないことが証明されているから，何らかの$ z_m R z_{m+1}に行かなければならない．しかし$ z_mは終末点，すなわち，そのような$ z_{m+1}は存在しないから，破綻してしまう．
よって更新することは出来ない．任意の$ nで$ H(n) = 0．